protocol race_DiamondRule1 {

child:
    async Msg1();
    async Msg1_();
parent:
    async Msg2();
    async Msg2_();

    // OK: this state machine is one of the simplest that follows the
    // Diamond Rule

start state S1:
    send Msg1 goto S2;
    recv Msg2 goto S3;

state S2:
    recv Msg2 goto S4;
    recv Msg2_ goto S2;

state S3:
    send Msg1 goto S4;
    send Msg1_ goto S3;

state S4:
    send Msg1 goto S4;
};
